perm filename AFC.PAP[VLI,LSP] blob
sn#381924 filedate 1978-09-08 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00006 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .right margin 72
C00007 00003 2. LE SYSTEME CAN.
C00013 00004 3. NECESSITE D'UN LANGAGE PARTICULIER.
C00019 00005 4. UN EXEMPLE COMPLET.
C00031 00006 .page
C00035 ENDMK
C⊗;
.right margin 72
.skip 4
.center;COMPREHENSION VISUELLE DE PROGRAMMES
.center;CONTROLEE PAR META-FILTRAGE
.skip 4
.center;Daniel GOOSSENS
.center;Departement d'informatique
.center;Universite PARIS 8
.center;Route de la Tourelle
.center;75012 PARIS
.center;RT-9-78##Juillet 1978
.skip 4
1. INTRODUCTION.
.skip 2
##Les rapports des programmeurs avec les systemes qu'ils implementent
posent de plus en plus de problemes, a mesure que ces systemes se
complexifient au point de ne pouvoir etre apprehendes que par aspects
partiels. Il devient alors urgent de construire des outils d'aide a la
mise au point. De tels outils doivent etre capables de comprendre suffisamment
les systemes qui leur sont fournis pour d'une part conseiller l'utilisateur
dans ses demarches et d'autre part empecher des actions visiblement
irrelevantes, voire nuisibles, sur ces systemes.
.skip 1
##Les travaux sur la verification de programmes (HOARE LAUER 1975, IGARASHI
LONDON LUCKHAM 1975) ne rentrent pas directement dans ce cadre car les
systemes de verification qu'ils ont engendre n'ont que la possibilite de
verifier ce que le programmeur veut verifier. Il n'est pas possible,
par exemple, de demander a de tels systemes de simplement
"comprendre" un programme, ou d'y "deceler les erreurs manifestes"
(calcul infini, portions de code non utilisees, redondances, indefinitions)
.break
##De recents travaux (GREEN BARSTOW 1975, RICH SHROBE 1975) ont produit
des systemes d'aide a la mise au point qui utilisent un grand nombre
de connaissances particulieres concernant les programmes qu'ils doivent
traiter. Si ces systemes a connaissances particulieres permettent des
resultats etonnants sur des programmes complexes, ils peuvent se
reveler totalement inefficaces sur des programmes simples hors du
domaine des connaissances particulieres.
.skip 1
##Ce qui manque a ces systemes d'aide a la mise au point, c'est un
processus de comprehension des enonces d'un langage de programmation,
c'est a dire un processus de traduction de ces phrases dans une forme
plus adequate aux travaux ulterieurs tels que decel et correction
d'erreurs. Nous avons grand besoin d'un processus de traduction
de la forme quelconque d'une phrase dans une representation plus
proche de son sens, voire une representation canonique de son sens.
.break
Il est en effet permis de penser que l'importance de la technologie
requise par les systemes actuels d'aide a la mise au point est
directement reliee a la diversite des facons de representer un sens
dans un langage de programmation.
.skip 3
2. LE SYSTEME CAN.
.skip 2
##Le systeme CAN est un meta-interprete. Il meta-evalue le corps
des programmes dans un environnement abstrait(1) (KING 1975,
BOYER ELSPASS LEVITT 1975, WERTZ 1978, HEWITT 1975, BALZER
GOLDMAN WILE 1977).
.footnote 4
------------------------------------------------------------------------
(1) Si ce dernier ne lui est pas fourni par le programmeur,
il construit l'environnement abstrait le plus general
possible.
.end footnote
.skip 1
##Pour mener a bien l'execution symbolique d'un enonce, CAN utilise
les definitions qu'il possede (en langage CAN), des fonctions qui
composent l'enonce. Lorsqu'il ne possede que la definition LISP
d'une de ces fonctions, il est capable dans de nombreux cas, de
synthetiser la definition CAN de cette fonction. Le resultat de la
meta-interpretation d'un programme est soit sa traduction complete en CAN,
ce qui correspond, dans le systeme CAN, a la comprehension complete du
programme, soit une traduction incomplete, redigee dans une
extension de CAN: le langage CAN*.
.skip 1
Le processus de meta-evaluation comprend 3 phases:
.skip 1
a) Confrontation.
.skip 1
##Pour comprendre une structure applicative, (F#A1#A2#...#An), le
systeme CAN doit d'abord comprendre les arguments A1#A2#...#An.
Ce qu'il comprend de ces arguments doit alors etre confronte a la
definition de F pour:
.skip 1
- Determiner a quelles conditions F peut s'appliquer sur ces
arguments.
.skip 1
- Extraire les caracteristiques de ces arguments (du moins de ce que
le systeme a pu en comprendre), necessaires a la construction de la valeur
ramenee par F et a l'expression des changements occasionnes par F sur son
environnement.
.skip 2
b) Propagation.
.skip 1
##Les renseignements recuperes lors de la phase de confrontation
sont propages partout. Cette phase sert notamment a construire la
valeur ramenee par une fonction et a exprimer les changements dans
l'environnement.
.skip 2
c) Generalisation.
.skip 1
##Les deux premieres phases permettent au systeme de lire
des portions de code a la maniere d'un interprete classique, si ce n'est
que le systeme evalue les fonctions dans un environnement abstrait.
Ce processus n'a pas de raison de s'arreter lors de l'interpretation de
structures iteratives ou recursives (KING 1975). Il faut un 3ieme
processus. La generalisation consiste a construire l'environnement
qui resulterait apres n evaluations d'une portion de code.
.skip 3
##Les 2 premieres phases se retrouvent dans la majorite des travaux
sur la meta-evaluation. La 3ieme est generalement remplacee par
la recherche d'un invariant de boucle (BOYER ELSPASS LEVITT 1975).
Le resultat d'une generalisation est une definition CAN de meme
nature que celles que le systeme possede deja. L'avantage de cette
phase de generalisation est qu'elle garde une unite au processus
de meta-interpretation.
.skip 1
##L'originalite du systeme CAN reside dans le mode de representation
des donnees abstraites (environnements, valeurs). Les donnees sont
representees "directement", sous forme "conceptuelle" (YONEZAWA
HEWITT 1976), plutot qu'indirectement, sous forme de relations.
Ces representations conceptuelles sont des FILTRES (GREUSSAY 1977).
Toute confrontation entre filtres se fait par l'intermediaire
d'un processus d'unification appele META-FILTRAGE (GOOSSENS 1978)
qui tient compte de la presence de "variables de segment contraintes".
.skip 3
3. NECESSITE D'UN LANGAGE PARTICULIER.
.skip 2
.nofill
(DE DERNIER-X (X L M)
(IF L (DERNIER-X X (CDR (MEMBER X L)) L)
M))
1
.fill
Si l'on representait les donnees abstraites directement sous LISP,
on meta-evaluerait: (DERNIER-X x l m).i:e: on meta-interpreterait
le corps de DERNIER-X dans l'environnement abstrait: X#=#x,#L#=#l,#M#=#m.
.skip 1
.nofill
2 cas:
l = nil le resultat est m
l = nil le resultat est
(DERNIER-X x (CDR (MEMBER x l)) l)
2 cas:
(CDR (MEMBER x l)) = NIL le resultat est l
(CDR (MEMBER x l)) = NIL le resultat est
(DERNIER-X x
(CDR
(MEMBER x
(CDR (MEMBER x l))))
(CDR (MEMBER x l)))
2 cas:
etc...
.fill
##La question est de savoir si (CDR (MEMBER x (CDR (MEMBER x l)))), par exemple,
est une bonne description d'un des resultats possibles, si cette forme est
une bonne representation de son sens.
.page
Imaginons l'implementation suivante de la fonction MEMBER:
.nofill
(DE MEMBER (X L)
(IF (AND L
(NOT (EQUAL (CAR L) X)))
(CONS (CAR L)
(MEMBER X (CDR L)))))
dont la fonction peut etre ainsi schematisee:
si L = (... x ...) et X = x le resultat est (...)
si L = (...) le resultat est (...)
(sans la presence de x)
2
.fill
Dans ce cas, l'ecriture (MEMBER x (CDR (MEMBER x l))) se simplifie.
En effet, (MEMBER x l) ramene une liste qui ne contient pas x. Le
CDR de cette liste ne contient donc pas non plus x. Or, l'action de
MEMBER sur une liste qui ne contient pas x est nulle, puisque dans
ce cas, MEMBER ramene la liste inchangee.
D'ou:
.nofill
(CDR (MEMBER x (CDR (MEMBER x l)))) = (CDR (CDR (MEMBER x l)))
.fill
Dans ce contexte, le programme DERNIER-X se contente de parcourir une
liste jusqu'a ce qu'elle soit vide. Pour qu'un systeme de verification
(HOARE 1973, IGARASHI 1975) puisse se rendre compte de cette inutilite du
calcul de DERNIER-X, il faut qu'il puisse d'une part prouver les
theoremes:
.nofill
(MEMBER x (CDR (MEMBER x l))) = (CDR (MEMBER x l))
(MEMBER x
(CDR (MEMBER x
(CDR (MEMBER x l)))))
= (MEMBER x
(CDR (CDR (MEMBER x l))))
= (CDR (CDR (MEMBER x l)))
et en general:
(MEMBER x (NTH nb (MEMBER x l)))
= (NTH nb (MEMBER x l))
.fill
et surtout, d'autre part, considerer auparavant ce theoreme particulier.
Or, pour ce faire, il faudrait qu'il ait DEJA compris quelque peu les
programmes MEMBER et DERNIER-X. Une telle verification ne peut donc
pas etre consideree comme de la comprehension, mais comme une
application de la comprehension.
.skip 1
Pour mener a bien une telle comprehension, il faut un processus
different.
.skip 1
C'est l'objet du systeme CAN que nous allons appliquer au meme exemple, et pour
le meme travail: examiner, sans autre directive, le programme##1##.
.skip 3
4. UN EXEMPLE COMPLET.
.skip 2
##Le corps de DERNIER-X est meta-interprete dans l'environnement general:
.skip 1
.nofill
X = !x L = !l M = !m
.fill
.skip 1
Le "!" indique que le domaine de definition de la variable est l'ensemble des
elements LISP. La definition en CAN* de IF fait envisager 2 cas selon l:
.skip 1
.nofill
L = NIL, X = !x, M = !m la valeur ramenee est !m
L = ( NIL !l), X = !x, M = !m
CAN doit comprendre: (DERNIER-X X (CDR (MEMBER X L)) L)
.fill
La forme "(##filtre1 filtre2)" equivaut a "filtre2". (##filtre1#...)
est une propriete de filtre2.
.break
MEMBER, dont la definition en CAN est (comparer avec##2##):
.skip 1
.nofill
((MEMBER !X !L)
(REF ((CAN !X)(CAN !L))
(!1 ((L ( !1 !2 )))) ---> ((L ( !1 !2 )))
(!1 ((L ( !1 !2 )) !1 ?3))
---> ((L ( !1 !2 )))))
.fill
est applique sur !x et ( NIL !l). (MEMBER !X !L) est l'aspect
syntaxique de MEMBER. Dans (REF forme ...), forme est le patron
a construire et a prendre en reference. Ici, (CAN !X) par exemple,
doit etre remplace par la comprehension par CAN de l'expression LISP
associee a !X, lors du filtrage de (MEMBER !X !L) avec une portion
de code. Le patron construit est alors compare (unifie) par
meta-filtrage, avec chacun des filtres gauches des regles qui
suivent. La forme (L##(##!1#!2#)) equivaut a: !2##!2##...!2#, ou
chaque !2## est different de !1. Le signe "?" indique une variable
de sequence.
.break
Dans le premier cas, (!x#(##NIL#!l)) #3##est unifie avec
(!1#((L##(##!1#!2#)))), ce qui donne les associations:
.skip 1
.nofill
!1 = !x, !l = ((L ( !x !2 )))
par propagation des resultats, la valeur de MEMBER est
((L ( !x !2 ))) 4
.fill
Dans le second cas,##3##est unifie avec (!1#((L##(##!1#!2#))#!1#?3)),
ce qui donne les associations:
.skip 1
.nofill
!1 = !x, !l = ((L ( !x !2 )) !x ?3)
la valeur de MEMBER est: ((L ( !x !2 ))) 4
.fill
Par le meme processus, dans les deux cas, grace a la definition CAN de
CDR:
.skip 1
.nofill
((CDR !L) (REF (CAN !L)
() ---> ()
(!4 ?5) ---> (?5)))
.fill
.skip 1
le systeme construit la valeur de (CDR#(MEMQ#X#L)).##4##
ne peut etre unifie qu'avec (!4#?5), ce qui donne:
.skip 1
.nofill
n = a + 1, ?5 = (L ( !x !2 )), !4 = ( !x !2 )
.fill
.skip 1
Le systeme construit une definition provisoire de DERNIER-X:
.skip 1
.nojustify
.nofill
1:(DERNIER-X !x () !m) = !m
2:(DERNIER-X !x (( !x !2 )(L ( !x !2 ))) !m)
= (DERNIER-X !x
((L ( !x !2 )))
(( !x !2 )(L ( !x !2 ))))
3:(DERNIER-X !X (( !x !2 )(L ( !x !2 )) !x ?3) !m)
= (DERNIER-X !x
((L ( !x !2 )))
(( !x !2 )(L ( !x !2 )) !x ?3))
.fill
.justify
.skip 1
##En considerant cette definition en CAN*, et en poursuivant le processus,
c'est a dire en meta-evaluant les appels recursifs, le systeme
se rend compte que ces appels ne peuvent "coincider" qu'avec les regles
1 et 2. Autrement dit, apres 1 appel recursif, la regle 3 n'a plus
de raison d'etre. Le 2ieme argument de DERNIER-X ne contient plus l'element
!x.
.break
Le systeme peut alors GENERALISER (GOOSSENS 1978) la regle 2:
.break
le meta-filtrage des filtres gauche (ou les variables sont primees
pour eviter toute confusion)
et droit de la regle 2 donne
les affectations:
.skip 1
.nojustify
.nofill
!x = !x, a = a + 1, ((L ( !x !2 ))) = (( !x !2 )(L ( !x !2 ))),
!m = (( !x !2 )(L ( !x !2 )))
.fill
.justify
.skip 1
Ces affectations peuvent alors etre considerees comme l'expression
d'une "distance" entre deux etats successifs de l'environnement.
Le systeme multiplie alors cette distance par un nombre fictif "nb":
.skip 1
.nojustify
.nofill
!x = !x, a = a + nb + 1,
((L ( !x !2 ))) = ((L ( !x !2 ))( !x !2 )(L ( !x !2 ))),
!m = (( !x !2 )(L ( !x !2 )))
.fill
.justify
.skip 1
A ce stade, la valeur de DERNIER-X est:
.skip 1
.nofill
(DERNIER-X !x ((L ( !x !2 ))) (( !x !2 )(L ( !x !2 ))))
.fill
.skip 1
Cet appel recursif est alors confronte a la seule regle "d'arret",
la regle 1.
.page
Par meta-filtrage:
.skip 1
.nofill
!x = !x, a = 0, !m = (( !x !2 ))
.fill
.skip 1
Par propagation sur !m, la valeur finale de DERNIER-X est
((##!x#!2##)), c'est a dire la liste du dernier element de son
second argument.
.break
Pour plus de rigueur, il faut egalement considerer le cas ou
la regle 3 coincide avec la regle 1, creant un cas particulier.
Dans ce cas, la valeur ramenee est le 2ieme argument en entier.
.break
Autrement dit, l'inutilite du calcul de DERNIER-X est revelee.
.skip 3
5. DISCUSSION.
.skip 2
##La propriete de canonicite des enonces CAN depend fortement de la
capacite du processus de META-FILTRAGE a unifier des filtres. Comme
nous ne connaissons pas de solution generale au probleme de
l'unification de filtres comportant des variables de segment, on ne
peut pretendre que chaque enonce CAN est la seule representation
de la fonction qu'il denote. Il s'agit plutot de tendre vers
cette propriete, en etendant a la fois le pouvoir descriptif du
langage CAN, et le domaine d'application du META-FILTREUR.
.break
##Ainsi, nous ne pensons pas qu'il faille chercher un unificateur
general, car bon nombre d'unifications ne sont pas naturelles, et
demanderaient, pour etre menees a bien, des techniques sophistiquees
de demonstration de theoremes. Un exemple est l'unification
de (?1 ?2) et (?2 ?1) dont le resultat est la comprehension de
(EQUAL (APPEND L M) (APPEND M L)).
.nofill
i:e: si L = ((L ?3)) et M = ((L ?3)) la valeur est T. NIL sinon.
.fill
##Pour CAN, il s'agit plutot de comprendre "directement" le plus
possible de ce qu'un programmeur considererait comme "visuellement
comprehensible".
.skip 3
6. CONCLUSION.
.skip 2
##Le langage CAN permet de decrire des fonctions de facon plus ou
moins precise. Voici par exemple 2 definitions de MEMBER:
.nofill
((MEMBER !X !L)
(REF ((CAN !X)(CAN !L))
(!1 (?2 !1 ?3)) ---> (!1 ?4)
(!1 ((L ( !1 !2)))) ---> NIL ))
((MEMBER !X !L)
(REF ((CAN !X)(CAN !L))
(!Y (?2)) ---> (?W) ))
.fill
.page
On peut donc avoir des renseignements plus ou mois generaux sur les
programmes que l'on soumet au systeme CAN suivant que l'on precise ou
non les definitions des fonctions de base.
.break
Dans le meme ordre d'idees, et sur une autre dimension, on peut
fournir une classe de donnees restreinte (sous forme de filtres)
sur laquelle meta-evaluer un programme. Autrement dit, l'interpretation
des programmes CAN est un cas particulier de leur meta-interpretation.
.break
C'est cette grande flexibilite d'utilisation qui fait de CAN un outil
d'aide a la mise au point d'une grande utilite.
.break
##CAN a deja traite de gros programmes (par exemple un algorithme
de filtrage) avec environ 50 definitions CAN de fonctions LISP de
base a sa disposition.
.break
##Il est ecrit en VLISP-10 (CHAILLOUX 1976, GREUSSAY 1976) et occupe
environ 10000 doublets LISP.
.page
7. BIBLIOGRAPHIE.
.skip 2
.nojustify
.nofill
BALZER, GOLDMAN ←& WILE (1977)
"Meta-evaluation as a tool for program
understanding"
5th IJCAI, MIT Cambridge, August 1977
BOYER, ELSPASS ←& LEVITT (1975)
"SELECT--A formal system for testing and
debugging programs by symbolic execution"
Int. Conf. on Reliable Software,
April 1975, pp. 234-245.
CHAILLOUX (1976) "VLISP-10 manuel de reference"
Dept. d'informatique, Univ. PARIS 8, RT 17-76.
GOOSSENS (1978) "A system for visual-like understanding of
LISP programs"
A.I.S.B. Conf. Hamburg, July 1978.
GREEN ←& BARSTOW (1975)
"A hypothetical dialogue exhibiting a
knowledge base for a program understanding
system"
Stanford A.I. Lab. MA 258, Cpt Science Dept.
Report n. Stancs-75-476.
GREUSSAY (1977) "Contribution a la definition interpretative et
a l'implementation des lambda-langages"
These, Universite PARIS 8.
HEWITT ←& SMITH (1975)
"Towards a programming apprentice"
IEEE Trans. on soft. engineering,
Vol. SE-1. pp. 26-45.
HOARE ←& LAUER (1973)
"Consistent and complementary formal theories
of the semantics of programming languages"
Ibid 3, pp. 145-182.
IGARASHI, LONDON ←& LUCKHAM (1975)
"Automatic program verification I: A logical
basis and its implementation"
Acta Informatica, Vol. 4, pp. 145-182.
KING (1975) "A new approach to program testing"
Int. Conf. on reliable software,
April 1975, pp. 228-233.
RICH ←& SCHROBE (1975)
"Understanding LISP programs: Towards a
programming apprentice"
Master's Thesis, EECS M.I.T.
WERTZ (1978) "Un systeme de comprehension, d'amelioration,
et de correction de programmes incorrects"
These de 3ieme cycle, Univ P. et M. CURIE.
YONEZAWA ←& HEWITT (1976)
"Symbolic evaluation using conceptual
representations for programs with
side-effects"
M.I.T., A.I. Lab., AI-Memo 399.
.fill